branch($P$;$d$;$p$.$A$($p$);$B$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$case $d$ of inl($p$) =$>$ $A$($p$) $\mid$ inr($x$) =$>$ $B$